Inference at * 2 
Iof proof for Lemma p-conditional-domain:



1. A : Type
2. B : Type
3. f : A(B + Top)
4. g : A(B + Top)
5. x : A
6. (isl(f(x)))  (isl(g(x)))
  isl(if isl(f(x)) then f(x) else g(x) fi ) 

latex

 by ((((D (-1)) 
CollapseTHEN (SplitOnConclITE))) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions	P  Q, left + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), P  Q, False, , , s = t, b, t  T, A, b, x:A. B(x)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, assert wf, bnot wf, not wf